(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


Require Import Reals.
Open Scope R_scope.
Require Export Matrix.Mat.RMatrix.
Require Export Matrix.Mat.RMtacs.
(** * Sa -> Sb *)
(* 迎角 α  (angle of attack) *)
Parameter alpha : R.
(* 侧滑角β (sidelip angle) *)
Parameter beta : R.
(* 由  气流坐标轴系(Sa)  转动侧滑角β到  稳定坐标轴系(Ss)*)
Definition coordinate_transform_SaSs:= mkMat_3_3
  (cos beta)    (- sin beta)   0
  (sin beta)    (cos beta)     0
     0           0             1.
(* 由 稳定坐标轴系 Ss 转动迎角 α 到 机体坐标轴系 Sb 的转换矩阵 *)
Definition coordinate_transform_SsSb := mkMat_3_3
  (cos alpha)   0  (- sin alpha)
      0         1        0
  (sin alpha)   0  (cos alpha).
Definition coordinate_transform_SaSb  := mkMat_3_3
  ((cos alpha)*(cos beta))  (-(cos alpha)*(sin beta))   (-sin alpha)
         (sin beta )              ( cos beta)                 0
  ((sin alpha)*(cos beta))  (-(sin alpha)*(sin beta))   (cos alpha).
(*Require Import Nsatz.*)
(* multiplication of SbSs and SsSa *)
Definition mul_SsSb_SsSa := 
  RMmul coordinate_transform_SsSb coordinate_transform_SaSs.
(* verify SsSa * SbSs = SbSa *)
Lemma SsSb_mul_SsSa_eq_SaSb : 
    mul_SsSb_SsSa === coordinate_transform_SaSb.
Proof.
  unfold mul_SsSb_SsSa.
  unfold coordinate_transform_SaSb.
  RMat_mul_simpl. unfold mkMat_3_3'.
  f_equal3. ring. f_equal2. ring.
Qed.